open util/boolean
sig date {
value: Int}

sig Cittadino {}

sig Politico extends Cittadino {
partito: one Partito }

sig Partito {}

sig PartecipazioneVotazione {
data: one date,
votante: one Cittadino }

sig VotoPolitica {
partitoVotato: one Partito,
preferenze: some Politico,
data: one date } {#preferenze<=3}

sig Elezione {
apertura: one date,
chiusura: one date}{apertura.value<chiusura.value}

sig PeriodoCandidatura{
inizio: one date,
fine: one date}{inizio.value<fine.value}

sig Candidatura{
politico: one Politico,
partito: one Partito,
data: one date}

fact TutteLeDateDopo20150101{
all d:date | d.value > 0}

fact DataValueUgualeImplicaStessaData{
no disjoint d1,d2: date | d1.value=d2.value}

fact NessunPartitoSenzaPolitici{
all par: Partito| some pol: Politico| par in pol.partito}

fact NessunPoliticoInPartitiDiversi{
all pol: Politico| no disjoint par1, par2: Partito | par1 in pol.partito && par2 in pol.partito }

fact NessunaCandidaturaAPoliticiDiversi{
all p: Politico | no disjoint c1,c2: Candidatura| p in c1.politico && p in c2.politico}

fact NessunaCandidaturaAPartitiDiversi{
all c: Candidatura| all p: Partito | p in c.partito implies p in c.politico.partito }

fact StessiNumeroDiVotantiEVoti{
#VotoPolitica = #PartecipazioneVotazione }

fact NoDoppiVoti{
no disjoint p1,p2: PartecipazioneVotazione | p1.votante = p2.votante}

fact VotiAiPoliticiDelloStessoPartito{
all v: VotoPolitica | all pol: v.preferenze | v.partitoVotato in pol.partito }

fact NessunVotoFuoriPeriodo{
all v:VotoPolitica | v.data.value >= Elezione.apertura.value && 
				        v.data.value <= Elezione.chiusura.value}

fact NessunaPartecipazioneFuoriPeriodo{
all p:PartecipazioneVotazione | p.data.value >= Elezione.apertura.value && 
									   p.data.value <= Elezione.chiusura.value }

fact NessunaCandidaturaFuoriPeriodo{
all c:Candidatura | c.data.value >= PeriodoCandidatura.inizio.value && 
						c.data.value <= PeriodoCandidatura.fine.value}

fact StessoNumeroCandidatureEPolitici{
#Candidatura = #Politico}

fact PeriodoCandidaturaPrecedenteAllaVotazione{
Elezione.apertura.value>PeriodoCandidatura.fine.value}


pred show()
{
#PeriodoCandidatura=1
#Elezione=1
#Politico = 4
#Partito = 2
#PartecipazioneVotazione =4
#Cittadino=5
#Candidatura=4 
#date=4
}
run show for 6



